\begin{tabbing}
$x$: $A$
\\[0ex]$a$: $B$
\\[0ex]rcv($l$,${\it tg}$) : $T$
\\[0ex]$a$(v) sends [${\it tg}$,   $f$($x$, v)] on link $l$  
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=with declarations \+
\\[0ex]ds:$x$ : $A$
\\[0ex]da:fpf{-}join(KindDeq;$a$ : $B$;rcv($l$,${\it tg}$) : $T$)
\\[0ex]$a$(v) sends $\langle$${\it tg}$$,\,$$\lambda$$s$,$v$. $f$($s$($x$),$v$)$\rangle$.nil s v on link $l$
\-
\end{tabbing}